(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_UFBV)
(declare-fun f0 ( (_ BitVec 10) (_ BitVec 15) (_ BitVec 15)) (_ BitVec 15))
(declare-fun f1 ( (_ BitVec 13) (_ BitVec 1)) (_ BitVec 3))
(declare-fun p0 ( (_ BitVec 5)) Bool)
(declare-fun v0 () (_ BitVec 2))
(declare-fun v1 () (_ BitVec 2))
(declare-fun v2 () (_ BitVec 14))
(declare-fun v3 () (_ BitVec 5))
(declare-fun v4 () (_ BitVec 5))
(assert (let ((e5(_ bv14 4)))
(let ((e6(_ bv58723 16)))
(let ((e7 (f1 ((_ zero_extend 8) v3) ((_ extract 1 1) v2))))
(let ((e8 (f0 ((_ sign_extend 6) e5) ((_ zero_extend 11) e5) ((_ extract 14 0) e6))))
(let ((e9 (bvnor v2 ((_ zero_extend 12) v1))))
(let ((e10 (bvmul ((_ sign_extend 12) v0) v2)))
(let ((e11 (ite (p0 ((_ zero_extend 1) e5)) (_ bv1 1) (_ bv0 1))))
(let ((e12 (ite (bvugt ((_ zero_extend 12) e5) e6) (_ bv1 1) (_ bv0 1))))
(let ((e13 (ite (bvslt v0 ((_ sign_extend 1) e11)) (_ bv1 1) (_ bv0 1))))
(let ((e14 ((_ repeat 10) e11)))
(let ((e15 (bvashr ((_ sign_extend 9) e12) e14)))
(let ((e16 (bvudiv e12 e13)))
(let ((e17 (ite (= (_ bv1 1) ((_ extract 0 0) e13)) e10 ((_ sign_extend 13) e16))))
(let ((e18 (bvxnor ((_ sign_extend 6) e5) e14)))
(let ((e19 (concat e13 e13)))
(let ((e20 ((_ rotate_right 2) e14)))
(let ((e21 (ite (bvule v2 ((_ sign_extend 13) e13)) (_ bv1 1) (_ bv0 1))))
(let ((e22 ((_ rotate_right 4) e14)))
(let ((e23 (ite (bvsle ((_ sign_extend 12) v1) e9) (_ bv1 1) (_ bv0 1))))
(let ((e24 (ite (p0 ((_ extract 9 5) e8)) (_ bv1 1) (_ bv0 1))))
(let ((e25 (bvmul v0 ((_ sign_extend 1) e21))))
(let ((e26 (bvneg e8)))
(let ((e27 ((_ extract 13 4) v2)))
(let ((e28 (ite (bvult e7 ((_ sign_extend 2) e24)) (_ bv1 1) (_ bv0 1))))
(let ((e29 ((_ zero_extend 1) e12)))
(let ((e30 (bvmul e10 e17)))
(let ((e31 (bvudiv ((_ zero_extend 4) e14) e10)))
(let ((e32 (f0 ((_ extract 11 2) e9) ((_ zero_extend 10) v4) ((_ sign_extend 13) e19))))
(let ((e33 (bvslt ((_ zero_extend 13) e21) v2)))
(let ((e34 (bvsle ((_ sign_extend 5) v3) e15)))
(let ((e35 (bvule e25 ((_ zero_extend 1) e12))))
(let ((e36 (p0 ((_ extract 5 1) e8))))
(let ((e37 (bvsgt v4 ((_ zero_extend 3) v1))))
(let ((e38 (bvsgt ((_ zero_extend 13) e12) e31)))
(let ((e39 (p0 ((_ zero_extend 4) e21))))
(let ((e40 (bvsgt e30 ((_ zero_extend 4) e22))))
(let ((e41 (bvule ((_ sign_extend 1) e28) e29)))
(let ((e42 (bvsle ((_ sign_extend 4) e12) v4)))
(let ((e43 (p0 ((_ extract 11 7) e32))))
(let ((e44 (distinct e6 ((_ sign_extend 6) e22))))
(let ((e45 (bvsgt ((_ sign_extend 5) e20) e26)))
(let ((e46 (bvsgt ((_ zero_extend 13) e28) e30)))
(let ((e47 (= e27 ((_ zero_extend 9) e28))))
(let ((e48 (bvule ((_ zero_extend 8) e19) e27)))
(let ((e49 (bvslt v2 ((_ sign_extend 9) v4))))
(let ((e50 (distinct ((_ sign_extend 9) e28) e14)))
(let ((e51 (bvslt ((_ zero_extend 14) e13) e32)))
(let ((e52 (bvugt e9 ((_ sign_extend 4) e27))))
(let ((e53 (distinct e10 ((_ zero_extend 10) e5))))
(let ((e54 (bvsgt e22 e27)))
(let ((e55 (bvsge e19 ((_ zero_extend 1) e23))))
(let ((e56 (bvsge e26 ((_ sign_extend 14) e23))))
(let ((e57 (bvsge e15 ((_ sign_extend 9) e21))))
(let ((e58 (bvuge e15 ((_ sign_extend 8) e29))))
(let ((e59 (bvule e30 e17)))
(let ((e60 (bvugt v4 ((_ sign_extend 4) e12))))
(let ((e61 (= ((_ zero_extend 9) e11) e14)))
(let ((e62 (bvsge ((_ zero_extend 13) e13) e17)))
(let ((e63 (bvsle v2 ((_ zero_extend 12) e19))))
(let ((e64 (= ((_ sign_extend 4) e14) e10)))
(let ((e65 (bvugt ((_ zero_extend 8) e29) e15)))
(let ((e66 (distinct e17 ((_ zero_extend 13) e21))))
(let ((e67 (bvuge e6 ((_ zero_extend 14) e29))))
(let ((e68 (distinct ((_ zero_extend 1) e13) e25)))
(let ((e69 (bvuge v2 ((_ sign_extend 11) e7))))
(let ((e70 (bvuge ((_ zero_extend 2) e28) e7)))
(let ((e71 (bvsgt e30 ((_ zero_extend 13) e24))))
(let ((e72 (bvult e20 ((_ sign_extend 9) e16))))
(let ((e73 (bvsle ((_ zero_extend 9) e13) e20)))
(let ((e74 (bvslt ((_ zero_extend 6) e14) e6)))
(let ((e75 (distinct ((_ zero_extend 3) e23) e5)))
(let ((e76 (= ((_ sign_extend 12) e19) e17)))
(let ((e77 (bvult e16 e23)))
(let ((e78 (bvsge ((_ zero_extend 9) e23) e20)))
(let ((e79 (bvule v4 ((_ sign_extend 4) e13))))
(let ((e80 (bvuge ((_ zero_extend 13) e19) e32)))
(let ((e81 (bvuge e31 ((_ sign_extend 12) e29))))
(let ((e82 (p0 ((_ zero_extend 3) v1))))
(let ((e83 (bvsge v2 ((_ sign_extend 13) e24))))
(let ((e84 (bvuge ((_ sign_extend 6) e27) e6)))
(let ((e85 (bvslt e6 ((_ zero_extend 6) e22))))
(let ((e86 (bvsle ((_ zero_extend 4) e21) v3)))
(let ((e87 (bvugt e13 e13)))
(let ((e88 (bvult ((_ zero_extend 9) e16) e18)))
(let ((e89 (bvslt ((_ zero_extend 3) v1) v3)))
(let ((e90 (bvule e9 ((_ sign_extend 12) e19))))
(let ((e91 (p0 ((_ extract 10 6) e26))))
(let ((e92 (bvuge e30 ((_ zero_extend 12) e19))))
(let ((e93 (p0 ((_ sign_extend 4) e12))))
(let ((e94 (bvsge ((_ zero_extend 4) e14) e10)))
(let ((e95 (bvugt ((_ sign_extend 11) v3) e6)))
(let ((e96 (distinct ((_ sign_extend 2) v1) e5)))
(let ((e97 (bvsge e24 e23)))
(let ((e98 (distinct e8 ((_ sign_extend 5) e27))))
(let ((e99 (bvult e28 e12)))
(let ((e100 (bvult ((_ zero_extend 1) v1) e7)))
(let ((e101 (bvugt ((_ sign_extend 9) e11) e14)))
(let ((e102 (bvule v0 ((_ zero_extend 1) e11))))
(let ((e103 (not e52)))
(let ((e104 (and e103 e78)))
(let ((e105 (= e39 e37)))
(let ((e106 (=> e100 e46)))
(let ((e107 (ite e104 e50 e59)))
(let ((e108 (and e96 e56)))
(let ((e109 (ite e55 e76 e51)))
(let ((e110 (and e99 e45)))
(let ((e111 (=> e69 e48)))
(let ((e112 (or e91 e84)))
(let ((e113 (= e60 e40)))
(let ((e114 (= e53 e47)))
(let ((e115 (ite e108 e113 e98)))
(let ((e116 (=> e42 e38)))
(let ((e117 (or e58 e62)))
(let ((e118 (xor e111 e102)))
(let ((e119 (xor e68 e35)))
(let ((e120 (and e117 e115)))
(let ((e121 (= e44 e118)))
(let ((e122 (= e34 e57)))
(let ((e123 (xor e83 e85)))
(let ((e124 (or e49 e101)))
(let ((e125 (ite e79 e43 e87)))
(let ((e126 (xor e86 e74)))
(let ((e127 (ite e67 e120 e73)))
(let ((e128 (=> e41 e81)))
(let ((e129 (not e65)))
(let ((e130 (and e123 e128)))
(let ((e131 (xor e77 e75)))
(let ((e132 (=> e119 e124)))
(let ((e133 (not e125)))
(let ((e134 (or e71 e64)))
(let ((e135 (or e122 e61)))
(let ((e136 (not e109)))
(let ((e137 (=> e135 e54)))
(let ((e138 (ite e33 e129 e116)))
(let ((e139 (ite e136 e89 e138)))
(let ((e140 (not e70)))
(let ((e141 (ite e92 e88 e133)))
(let ((e142 (xor e112 e137)))
(let ((e143 (=> e90 e72)))
(let ((e144 (ite e134 e142 e95)))
(let ((e145 (not e80)))
(let ((e146 (not e140)))
(let ((e147 (not e110)))
(let ((e148 (ite e143 e93 e97)))
(let ((e149 (xor e94 e82)))
(let ((e150 (=> e131 e141)))
(let ((e151 (not e114)))
(let ((e152 (or e63 e106)))
(let ((e153 (ite e132 e151 e149)))
(let ((e154 (or e146 e148)))
(let ((e155 (=> e154 e107)))
(let ((e156 (xor e150 e105)))
(let ((e157 (xor e144 e147)))
(let ((e158 (not e145)))
(let ((e159 (and e126 e157)))
(let ((e160 (and e127 e36)))
(let ((e161 (or e152 e121)))
(let ((e162 (xor e139 e139)))
(let ((e163 (and e66 e155)))
(let ((e164 (xor e156 e159)))
(let ((e165 (ite e161 e153 e161)))
(let ((e166 (ite e163 e165 e165)))
(let ((e167 (= e158 e164)))
(let ((e168 (or e130 e162)))
(let ((e169 (=> e167 e160)))
(let ((e170 (ite e168 e169 e169)))
(let ((e171 (and e166 e170)))
(let ((e172 (and e171 (not (= e13 (_ bv0 1))))))
(let ((e173 (and e172 (not (= e10 (_ bv0 14))))))
e173
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
